Nuprl Lemma : free-from-atom-rational
11,40
postcript
pdf
a
:Atom1,
q
:
.
q
:
||
a
latex
Definitions
x
:
A
.
B
(
x
)
,
,
t
T
,
a
b
T
,
x
:
A
.
B
(
x
)
,
A
c
B
,
,
P
Q
Lemmas
q-elim
,
int
nzero
properties
,
nequal
wf
,
free-from-atom
wf1
,
rationals
wf
,
qdiv
wf
,
int-rational
,
int
nzero-rational
,
free-from-atom-int
origin
a:Atom1, q:
. q:||a a:Atom1, q:. q:||a x:A. B(x)
T
b T 
x:A. B(x)
B
Q